sample.c

typedef /*@abstract@*/ char *mstring;
 
int faucet (void)
{
  int *x = (int *) malloc (sizeof (int) * 24);
 
  /*
  ** silly program ...
  */
 
  return 3;
}